T:Type, f:(TT), n:, x:T. f(f^n(x)) = f^n+1(x) 

latex

Definitions	, t  T, f o g, x:A. B(x), False, P  Q, A, A  B, , {T}, SQType(T), ff, tt, (i = j), if b then t else f fi , Y, primrec(n;b;c), f^n
Lemmas	nat wf, fun exp wf, le wf, fun exp add, compose wf